q-sat-constraints(k;A;y)
== (||y|| = k)
== c (aA.
== c (let F,r,G = a in 
== c (if (r = 0)
== c (ifthen q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y)
== c (if (r = 1)
== c (ifthen q-linear(k;j.F[j]?0;y)  q-linear(k;j.G[j]?0;y)
== c (else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
== c (fi ) 

latex

---

clarification:

q-sat-constraints(k;A;y)
== (||y|| = k  )
== c l_all(A;:( List)  (:  ( List));a.let F,r,G = a in 
== c l_all(A;:( List)  (:  ( List));a.if (r = 0)
== c l_all(A;:( List)  (:  ( List));a.ifthen q-linear(k;j.F[j]?0;y)
== c l_all(A;:( List)  (:  ( List));a.ifthen =
== c l_all(A;:( List)  (:  ( List));a.ifthen q-linear(k;j.G[j]?0;y)
== c l_all(A;:( List)  (:  ( List));a.ifthen  
== c l_all(A;:( List)  (:  ( List));a.if (r = 1)
== c l_all(A;:( List)  (:  ( List));a.ifthen q-linear(k;j.F[j]?0;y)  q-linear(k;j.G[j]?0;y)
== c l_all(A;:( List)  (:  ( List));a.else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
== c l_all(A;:( List)  (:  ( List));a.fi ) 

latex

Definitions	A c B, ||as||, xL. P(x), x:A  B(x), , type List, let x,y,z = a in t(x;y;z), s = t, , if b then t else f fi , (i = j), r  s, r < s, q-linear(k;i.X(i);y), as[i]?a, #$n
FDL editor aliases	q-sat-constraints